Forward proofs.md (2413B)
1 +++ 2 title = 'Forward proofs' 3 +++ 4 # Forward proofs 5 ## Structured constructs 6 Structured proofs are Lean's proof terms with syntactic sugar. 7 Simplest kind is lemma, possibly with argument: 8 9 ```lean 10 lemma add_comm (m n : Ν) : 11 add m n = add n m := 12 sorry 13 ``` 14 15 `fix` and `assume`: move `∀`-quantified vars/assumptions from goal into local context (like `intros`) 16 `show g, from ...`: repeats goal to prove, can also be used to rephrase goal including computation 17 `have h := ...` proves intermediate lemma 18 `let...in` introduces a variable 19 20 You can enter tactic mode (backward reasoning) by using `begin..end` blocks, e.g. in a `from` 21 22 ## Calculational proofs 23 Sometimes we use transitive chains of relations (e.g. `a ≥ b ≥ c`). 24 In lean, you use `calc`: 25 26 ```lean 27 lemma two_mul (m n : Ν) : 28 2 * m + n = m + n + m := 29 calc 2 * m + n 30 = (m + m) + n : 31 by rw two_mul 32 ... = m + n + m : 33 by cc 34 ``` 35 36 ## Dependent types 37 For example, have a function `pick` taking natural number n as argument, and returning number between 0 and n. 38 This means that `pick` has a dependent type: `(n : Ν) → {i : Ν | i ≤ n}` (`|` is "such that", in lean it's `//`) 39 40 A "dependent type" means type depending on another term. 41 42 In lean, you write a dependent type `(x : σ) → τ` as `∀x : σ, τ` 43 44 ## Curry-Howard Correspondence 45 PAT = propositions as types = proofs as terms 46 47 That is, the same lemma can be proved in multiple ways. 48 49 As a function: 50 51 ```lean 52 lemma and_swap (a b : Prop) : 53 a ∧ b → b ∧ a := 54 λhab : a ∧ b, and.intro (and.elim_right hab) (and.elim_left hab) 55 ``` 56 57 As a tactical proof: 58 59 ```lean 60 lemma and_swap (a b : Prop) : 61 a ∧ b → b ∧ a := 62 begin 63 intro hab, 64 apply and.intro, 65 apply and.elim_right, 66 exact hab, 67 apply and.elim_left, 68 exact hab 69 end 70 ``` 71 72 As a structured proof: 73 74 ```lean 75 lemma and_swap (a b : Prop) : 76 a ∧ b → b ∧ a := 77 assume hab : a ∧ b, 78 have hb : b := 79 and.elim_right hab, 80 show b ∧ a, from 81 and.intro hb (and.elim_left hab) 82 ``` 83 84 ## Induction by pattern matching 85 Curry-Howard also means that proof by induction is like a recursively specified proof term. 86 The induction hypothesis is then the name of the lemma we're proving. 87 88 ```lean 89 lemma reverse_append {α : Type} : 90 ∀xs ys : list α, reverse (xs ++ ys) = reverse ys ++ reverse xs 91 | [] ys := by simp [reverse] 92 | (x :: xs) ys := by simp [reverse, reverse_append xs ys] 93 ```